package controller.solver;

import java.io.BufferedReader;
import java.io.File;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.Scanner;
import java.util.concurrent.Semaphore;

import model.ParameterValue;
import model.solver.ESolver;
import model.solver.MiniSatParameter;
import model.solver.SolverParameter;
import model.solver.SolverResult;
import model.solver.SolverResultStatus;

/**
 * This class is a implementation of Solver for Minisat.
 * 
 * @author GRONOWSKI Stephane svan001@aol.com
 * 
 *         igsat 2010
 * 
 */
public class MiniSat extends Solver {

	public static final String	EXEC					= "minisat";
	public static final String	DESCRIPTION				= "Result of the minisat execution";

	public static final String	RESTARTS_TOKEN			= "restarts";
	public static final String	DECISIONS_TOKEN			= "decisions: ";
	public static final String	CONFLICTS_TOKEN			= "conflicts: ";
	public static final String	PROPAGATIONS_TOKEN		= "propagations";
	public static final String	CINF_LITTERALS_TOKEN	= "conflict literals";
	public static final String	MEMORY_TOKEN			= "Memory used";

	// public static final int DEFAULT_RETURN_VALUE = 0;

	/** The default value that is associate to a UNSATISFIABLE result */
	public static final int		RETURN_UNSATISFIABLE	= 20;
	/** The default value that is associate to a SATISFIABLE result */
	public static final int		RETURN_SATISFIABLE		= 0;

	private MiniSatParameter	param;

	/**
	 * Create a Minisat solver.
	 * 
	 * @param directory
	 *            directory where the executable file is.
	 * @throws IOException
	 *             if there is a problem with the file.
	 */
	public MiniSat(File directory) throws IOException {
		if (!directory.isDirectory() || !new File(directory, EXEC).isFile())
			throw new IllegalArgumentException();

		param = new MiniSatParameter();
		type = ESolver.MINISAT;

		try
		{
			path = directory.getCanonicalPath() + File.separator + EXEC;
		} catch (IOException e)
		{
			e.printStackTrace();
			throw new IOException();
		}
	}

	/**
	 * 
	 * 
	 * @return the {@link MiniSatParameter}
	 */
	public MiniSatParameter getMiniSatParameter() {
		return param;
	}

	@Override
	public boolean checkParameter() {
		return param.basicCheck();
	}

	@Override
	public SolverParameter getSolverParameter() {
		return param;
	}

	@Override
	public String[] getCommandLine(String cnfFile) {
		String[] tab = new String[2 + param.getCommandLineNbParameterSup()];

		// path
		tab[0] = path;
		// satellite
		if (param.isPre())
			tab[1] = "-pre=once";
		else
			tab[1] = "-pre=none";

		int nb = 2;
		// asym
		if (param.getAsymm() != ParameterValue.NOT_USED)
			tab[nb++] = "-asymm=" + param.getAsymm().getVal();
		// rcheck
		if (param.getRcheck() != ParameterValue.NOT_USED)
			tab[nb++] = "-rcheck=" + param.getRcheck().getVal();
		// grow
		if (param.getGrow() != MiniSatParameter.NOT_USED)
			tab[nb++] = "-grow=" + param.getGrow();
		// polarity
		if (param.getPolarityMode() != ParameterValue.NOT_USED)
			tab[nb++] = "-polarity-mode=" + param.getPolarityMode().getVal();
		// decay
		if (param.getDecay() != MiniSatParameter.NOT_USED)
			tab[nb++] = "-decay=" + param.getDecay();
		// rnd freq
		if (param.getRndfreq() != MiniSatParameter.NOT_USED)
			tab[nb++] = "-rnd-freq=" + param.getRndfreq();
		// rnd verbosity
		if (param.getVerbosity() != MiniSatParameter.NOT_USED)
			tab[nb++] = "-verbosity=" + param.getVerbosity();

		// stdin
		tab[nb] = cnfFile;// correctFormatForLinux(cnfFile);

		return tab;
	}

	@Override
	public boolean hasTimeout() {
		return false;
	}

	@Override
	public SolverResult runSolver(String[] cmd, Semaphore manager) {
		SolverResult res = new SolverResult();

		BufferedReader input = null;
		BufferedReader inerr = null;
		try
		{// lance le processus
			res.setBegin(System.currentTimeMillis());
			setRunning(true);

			try
			{
				process = Runtime.getRuntime().exec(cmd);
			} catch (IOException e)
			{
				throw e;
			}
			finally
			{// libere les sem
				sem.release();
				if (manager != null)
					manager.release();
			}

			String line;
			input = new BufferedReader(new InputStreamReader(process.getInputStream()));
			inerr = new BufferedReader(new InputStreamReader(process.getErrorStream()));

			while ((line = input.readLine()) != null)
			{ // verifie les stdin
				System.out.println(line);
				res.addStdin(line + "\n");
			}
			while ((line = inerr.readLine()) != null)
				// System.out.println(line);
				res.addStderr(line + "\n");
		} catch (IOException e)
		{
			// e.printStackTrace();
			res.setStatus(SolverResultStatus.PROBLEM);
			if (process != null)
				process.destroy();
		}
		finally
		{
			try
			{
				if (input != null)
					input.close();
				if (inerr != null)
					inerr.close();
				if (process != null)
					res.setExitVal(process.waitFor());
			} catch (Exception e)
			{
				// e.printStackTrace();
				res.setStatus(SolverResultStatus.PROBLEM);
			}
			finally
			{
				try
				{
					sem.acquire();
				} catch (InterruptedException e)
				{
					// TODO Auto-generated catch block
					e.printStackTrace();
					return null;
				}

				setRunning(false);
			}
		}
		// terminer
		res.setEnd(System.currentTimeMillis());

		// System.out.println("val de retour" + res.getExitVal());

		// s'occupe du status
		if (hasBeenStop())
			res.setStatus(SolverResultStatus.STOP);
		else
			if (hasBeenTimeout())
				res.setStatus(SolverResultStatus.TIMEOUT_REACHED);
			else
				if (res.getStatus() == SolverResultStatus.PROBLEM)
					switch (res.getExitVal()) {
					case RETURN_UNSATISFIABLE:
						res.setStatus(SolverResultStatus.UNSATISFIABLE);
						break;
					case RETURN_SATISFIABLE:
						res.setStatus(SolverResultStatus.SATISFIABLE);
						setLastResult(res);
						break;

					default:
						res.setStatus(SolverResultStatus.PROBLEM);
					}

		// dernier details
		res.setDescription(DESCRIPTION);

		sem.release();
		return res;
	}

	private void setLastResult(SolverResult res) {
		int index = res.getStderr().indexOf(RESTARTS_TOKEN);

		if (index == -1)
			return;

		// recupere la chaine de puis le token
		String out = res.getStderr().substring(index);
		// String pattern = "\\s*" + RESTARTS_TOKEN + "\\s*:\n\\s*" +
		// CONFLICTS_TOKEN + "\\s*:\n\\s*"
		Scanner scan = new Scanner(out);
		// restarts
		for (int i = 2 ; i > 0 ; i--)
			scan.next();
		res.setRestarts(scan.nextInt());
		// conflicts
		for (int i = 2 ; i > 0 ; i--)
			scan.next();
		res.setConflics(scan.nextInt());
		// decisions
		for (int i = 4 ; i > 0 ; i--)
			scan.next();
		res.setDecisions(scan.nextInt());
		// propagations
		for (int i = 7 ; i > 0 ; i--)
			scan.next();
		res.setPropagations(scan.nextInt());
		// conflic literal
		for (int i = 5 ; i > 0 ; i--)
			scan.next();
		res.setConflicLiterals(scan.nextInt());
		// memory used
		for (int i = 7 ; i > 0 ; i--)
			scan.next();
		res.setMemoryUsed(scan.next() + " " + scan.next());

	}

}
